Nuprl Lemma : fun_exp_add 11,40

T:Type, nm:f:(TT). f^n+m = (f^n o f^m TT 
latex


DefinitionsP  Q, P & Q, t  T, P  Q, P  Q, f^n, x:AB(x),
Lemmasint seg wf, compose wf, primrec add, fun exp compose, fun exp wf, nat wf

origin